$\forall$$T$:Type, ${\it dT}$:EqDecider($T$), $L$:($T$ List), $x$, $y$:$T$.
\\[0ex]($x$ $\in$ $L$) $\Rightarrow$ ($y$ $\in$ $L$) $\Rightarrow$ (index($L$;$x$) $<$ index($L$;$y$)) $\Rightarrow$ $x$ before $y$ $\in$ $L$